Inference at * 1 1 
Iof proof for Lemma fseg select:



1. T : Type
2. l1 : T List
3. l2 : T List
4. L : T List
5. l2 = (L @ l1)
6. i : 
7. i < ||l1||
  l1[i] = (L @ l1)[((||L @ l1|| - ||l1||)+i)] 

latex

 by ((((RWO "select_append_back" 0) 
CollapseTHENA (Auto))) 
CollapseTHEN ((((Try (((EqCD) 

CoCollapseTHEN (Auto))))) 
CollapseTHEN (((RWO "length_append" 0) 
CollapseTHEN (Auto'))))))
C 

latex

C.

Definitions	S  T, |g|, {i..j}, Void, i  j < k, l[i], #$n, , T, True, {x:A| B(x)} , A, False, -n, A  B, P  Q, P & Q, x:A  B(x), x:A. B(x), P  Q, P  Q, x:AB(x), , n+m, ||as||, as @ bs, a < b, , type List, Type, s = t, t  T, n - m
Lemmas	select append back, int seg wf, member wf, append wf, true wf, select wf, squash wf, le wf, length wf1, iff wf, rev implies wf, add functionality wrt eq, length append